\begin{tabbing}
$\forall$\=${\it ds}$:fpf(Id; $x$.Type), ${\it da}$:fpf(Knd; $k$.Type), $A$,$B$:ecl{-}trans{-}tuple\{i:l\}(${\it ds}$; ${\it da}$), $m$:$\mathbb{N}$,\+
\\[0ex]$L$:(event{-}info(${\it ds}$;${\it da}$) List), $z$:event{-}info(${\it ds}$;${\it da}$).
\-\\[0ex]spreadn(\=$A$;\+
\\[0ex]${\it Ta}$,${\it ksa}$,${\it ia}$,${\it ga}$,${\it ha}$,${\it aa}$,${\it ea}$.spreadn(\=$B$;\+
\\[0ex]${\it Tb}$,${\it ksb}$,${\it ib}$,${\it gb}$,${\it hb}$,${\it ab}$,${\it eb}$.((${\it Ta}$ = ${\it Tb}$ $\in$ Type)
\\[0ex]c$\wedge$ ((${\it ksa}$ = ${\it ksb}$ $\in$ (Knd List)) $\wedge$ (${\it ia}$ = ${\it ib}$ $\in$ ${\it Ta}$))
\\[0ex]c$\wedge$ \=((\=${\it aa}$\+\+
\\[0ex]=
\\[0ex]${\it ab}$
\\[0ex]$\in$ $\mathbb{N}\rightarrow$(\=$k$:\{$k$:Knd$\mid$ ($k$ $\in$ ${\it ksa}$)\} $\rightarrow$decl{-}state(${\it ds}$)$\rightarrow$\+
\\[0ex]ma{-}valtype(${\it da}$; $k$)$\rightarrow$${\it Ta}$$\rightarrow\mathbb{B}$))
\-\-\\[0ex]$\wedge$ \=(\=$\forall$${\it L'}$:(event{-}info(${\it ds}$;${\it da}$) List), $k$:\{\=$k$:Knd$\mid$ \+\+\+
\\[0ex]($k$ $\in$ ${\it ksa}$)\} ,
\-\\[0ex]$s$:decl{-}state(${\it ds}$), $v$:ma{-}valtype(${\it da}$; $k$).
\-\\[0ex]iseg(\=event{-}info(${\it ds}$;${\it da}$);\+
\\[0ex]append(${\it L'}$; cons($<$$k$, $s$, $v$$>$; []));
\\[0ex]$L$)
\-\\[0ex]$\Rightarrow$ (\=${\it gb}$($k$,$s$,$v$,ecl{-}trans{-}state($B$; ${\it L'}$))\+
\\[0ex]=
\\[0ex]${\it ga}$($k$,$s$,$v$,ecl{-}trans{-}state($B$; ${\it L'}$))
\\[0ex]$\in$ ${\it Ta}$))))))
\-\-\-\-\-\\[0ex]$\Rightarrow$ (ecl{-}trans{-}act(${\it ds}$; ${\it da}$; $A$)($m$,append($L$; cons($z$; []))))
\\[0ex]$\Rightarrow$ (ecl{-}trans{-}act(${\it ds}$; ${\it da}$; $B$)($m$,append($L$; cons($z$; []))))
\end{tabbing}